signature ASSEM_STRUCTS = 
sig
end

signature ASSEM = 
sig
  include ASSEM_STRUCTS
   
  datatype reg = Eax | Ebp | Ebx | Ecx | Edi | Edx | Esi | Esp

  type state

  datatype st
    = Rf of int
    | Hp of int
    | Upd of st * exp * exp 
  and exp
    = IntNum of int 
    | Mem of int
    | Id of string 
    | Plus of exp * exp 
    | Minus of exp * exp 
    | Times of exp * exp 
    | Sel of st * exp 
    | Reg of reg
    | Zf
    | Sf
    | Some of exp
    | State of state
    | TrForm of string * exp

  datatype etype
    = Int
    | Ptr of etype 
    | Str of string 
    | Wild 
 
  val setSt : {hp : st, rf : st} -> state
  val getRf : state -> st
  val getHp : state -> st
  val updRf : st * state -> state
  val updHp : st * state -> state
  val updSt : {rf : st, hp : st} * state -> state

  datatype prop 
    = True
    | Imply of prop * prop
    | Not of prop
    | And of prop * prop
    | Or of prop * prop
    | Gt of exp * exp
    | Ge of exp * exp
    | Lt of exp * exp
    | Le of exp * exp
    | Eq of exp * exp
    | Ne of exp * exp
    | Ex of (string * etype) * prop
    | Forall of (string * etype) * prop
    | Tree of st * exp * int * int * int 
    | List of st * exp * int * int 
    | InDomM of state * exp 
    | Pred of string * prop
    | GoodFrame of state * exp
    | Stack of state * state
    | NotInDomM of state * exp

  type assert = state -> state ->  prop

  type lab = string
  
  datatype sec = Data | Other of string | Text

  datatype aptr
    = Preg of reg  
    | Pstk of int * reg 
    | Pmem of int * aptr * pexp
    | Pgmem of int
    | Pid of string
  and pexp 
    = Pvar of aptr
    | PintNum of int
    | Pplus of pexp * pexp
    | Pminus of pexp * pexp
    | Ptimes of pexp * pexp

  datatype pprop
    = Ptrue
    | Pnot of pprop
    | Pand of pprop * pprop
    | Por of pprop * pprop
    | Pge of pexp * pexp
    | Pgt of pexp * pexp
    | Plt of pexp * pexp
    | Ple of pexp * pexp
    | Peq of pexp * pexp
    | Pne of pexp * pexp
    | Pforall of (string * etype) * pprop
    | Pex of (string * etype) * pprop
    | Pi of aptr list list
    | N of aptr list
    | D of aptr list
    | Ptree of pexp
    | Plist of pexp
    | Ppred of string * pprop

  type passert = pprop option
  type opta
  val newAsst : (assert * passert) option -> opta
  val newAsstMain : (assert * passert) option -> opta
  val getLabId : opta -> int


  val getLabA : opta -> (assert * passert) option
  
  val getLabAsst : opta -> assert option
  
  val getLabPasst : opta -> passert

  datatype instr
    = Addr of reg * reg
    | Addz of int * reg
    | Addm of int * reg * reg
    | Subr of reg * reg
    | Subz of int * reg
    | Subm of int * reg * reg
    | Mulr of reg * reg
    | Mulz of int * reg
    | Mulm of int * reg * reg
    | Div of reg

    | Movld of int * reg * reg
    | Movr of reg * reg
    | Movst of reg * int * reg
    | Movz of int * reg * etype

    | Xchg of reg * reg
    | Leab of int * reg * reg
    | Leal of lab * reg
    | Cmpr of reg * reg
    | Cmpz of int * reg
    | Pop of reg
    | Push of reg
    | Leave

    | Jg of lab * lab
    | Je of lab * lab
    | Jge of lab * lab
    | Jmp of lab
    | Call of lab * lab
    | Ret of lab

    | Section of sec
    | Label of string * opta
    | Directive of string
    | ExtrA of assert

    | Malloc of int * lab * etype
    | Free of reg

  datatype pf 
    = WfSeq of pf * string * (instr list) 
    | WfJmp of string * instr 
    | WfJg of string * string * instr
    | WfJe of string * string * instr
    | WfJge of string * string * instr
    | WfCall of string * string * instr
    | WfRet of string 
    | WfMalloc of string * instr

  type codeblk
  val getCbLab : codeblk -> string
  val getCbId : codeblk -> int
  val getCbCode : codeblk -> instr list
  val getCbAsst : codeblk -> assert option
  val getCbPf : codeblk -> (pf * string) option
  val setCbPf : codeblk * pf * string -> codeblk
  val getCbAlist : codeblk -> (string * assert) list
  val addCbAlist : codeblk * (string * assert) -> codeblk
  val getCbFstA : codeblk -> (string * assert)
  val setCbAsst : (codeblk * assert) -> codeblk

  val getCbPasst : codeblk -> passert
  
  val getCbA : codeblk -> (assert * passert) option
  
  val setCb : (string * int * instr list * (assert * passert) option * 
               (pf * string) option * (string * assert) list) -> codeblk 

  datatype arg
    = O of string
    | L of arg list
    | P of arg list

  datatype tactic
    = Tapply of string * ((string * string) list)
    | Tintros of (string list)
    | Tinversion_clear of string * (arg list)
    | Tproof
    | Tqed
    | Tauto
    | Tunfold of string
    | Tor of tactic * tactic
    | Tseq of tactic list
    | Tpara of (tactic list)
    | Tsplit
    | Texists of string
    | TexistsS of st * st
    | Trepeat of tactic
    | Tconstructor
    | Ttry of tactic
    | Tomega
    | TtacIn of tactic * string  
    | Tinduction of string * (arg list)
    | Tdestruct of string * (arg list)
    | Tsimpl
    | Tassert of string * prop
    | Tclear of string
    | Treflexivity
    | Treplace of exp * exp
    | Trewrite of string
    | Tinjection of string
    | Tcut of string

  type code4ptr
  val getCbLab4p : code4ptr -> string
  val getCbCode4p : code4ptr -> instr list
  val getCbAsst4p : code4ptr -> passert
  
  val setCb4p : string * instr list * passert -> code4ptr

  type pprf 
  type ginf
  type asmenv
  val getFname : pprf -> string
  val getCode : pprf -> code4ptr list
  val getAsmEnv : pprf -> asmenv
  val getType : aptr * asmenv -> etype option
  val getOtherEnvPtr : aptr * asmenv -> aptr 
  
  val getPre : pprf -> passert
  val getPost : pprf -> passert
  val setPprf : string * passert * passert * (code4ptr list) * (aptr * aptr * etype) list -> pprf
  
  val getStrType : ((string * int) * ginf) -> etype option
  val getStrFields : (string * ginf) -> (int * etype) list

  val getData : ginf -> instr list

  val getParas : pprf list * string -> (aptr * etype) list
  val getFRet : string * ginf -> etype
  
  val setGinf : ((string * (int * etype) list) list) * (instr list) * ((string * etype) list)-> ginf


  val toString : instr -> string

  val etype2str : etype -> string 
  
  val aptr2str: aptr -> string
  val aptrs2str : aptr list -> string

  val pexp2str : pexp -> string

  val pprop2str : pprop -> string
  
  val asmenv2str : asmenv -> string      
end
